Search Results

Documents authored by Poetzsch-Heffter, Arnd

Document
DOI: 10.4230/DagSemProc.09301.1
09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs

Authors: Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn

Published in: Dagstuhl Seminar Proceedings, Volume 9301, Typing, Analysis and Verification of Heap-Manipulating Programs (2010)

Abstract
From July 19 to 24, 2009, the Dagstuhl Seminar 09301 ``Typing, Analysis and Verification of Heap-Manipulating Programs '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn. 09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs. In Typing, Analysis and Verification of Heap-Manipulating Programs. Dagstuhl Seminar Proceedings, Volume 9301, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{sagiv_et_al:DagSemProc.09301.1,
  author =	{Sagiv, Mooly and Poetzsch-Heffter, Arnd and O'Hearn, Peter},
  title =	{{09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs}},
  booktitle =	{Typing, Analysis and Verification of Heap-Manipulating Programs},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9301},
  editor =	{Peter O'Hearn and Arnd Poetzsch-Heffter and Mooly Sagiv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09301.1},
  URN =		{urn:nbn:de:0030-drops-24361},
  doi =		{10.4230/DagSemProc.09301.1},
  annote =	{Keywords: Ownership types, static analysis, program verification, heap-manipulating programs}
}
Document
DOI: 10.4230/DagSemProc.09301.2
09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs

Authors: Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn

Published in: Dagstuhl Seminar Proceedings, Volume 9301, Typing, Analysis and Verification of Heap-Manipulating Programs (2010)

Abstract
The document contains an executive summary of the Dagstuhl Seminar "Typing, Analysis, and Verification of Heap-Manipulating Programs" that took place July 2009.
Cite as

Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn. 09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs. In Typing, Analysis and Verification of Heap-Manipulating Programs. Dagstuhl Seminar Proceedings, Volume 9301, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{sagiv_et_al:DagSemProc.09301.2,
  author =	{Sagiv, Mooly and Poetzsch-Heffter, Arnd and O'Hearn, Peter},
  title =	{{09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs}},
  booktitle =	{Typing, Analysis and Verification of Heap-Manipulating Programs},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9301},
  editor =	{Peter O'Hearn and Arnd Poetzsch-Heffter and Mooly Sagiv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09301.2},
  URN =		{urn:nbn:de:0030-drops-24354},
  doi =		{10.4230/DagSemProc.09301.2},
  annote =	{Keywords: Typing, Static Analysis, Verification, Heap-Manipulating Programs}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.699
Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Authors: Ina Schaefer and Arnd Poetzsch-Heffter

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
Self-adaptive embedded systems autonomously adapt to changing environment conditions to improve their functionality and to increase their dependability by downgrading functionality in case of fail- ures. However, adaptation behaviour of embedded systems significantly complicates system design and poses new challenges for guaranteeing system correctness, in particular vital in the automotive domain. Formal verification as applied in safety-critical applications must therefore be able to address not only temporal and functional properties, but also dynamic adaptation according to external and internal stimuli. In this paper, we introduce a formal semantic-based framework to model, specify and verify the functional and the adaptation behaviour of syn- chronous adaptive systems. The modelling separates functional and adap- tive behaviour to reduce the design complexity and to enable modular reasoning about both aspects independently as well as in combination. By an example, we show how to use this framework in order to verify properties of synchronous adaptive systems. Modular reasoning in com- bination with abstraction mechanisms makes automatic model checking efficiently applicable.
Cite as

Ina Schaefer and Arnd Poetzsch-Heffter. Using Abstraction in Modular Verification of Synchronous Adaptive Systems. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{schaefer_et_al:OASIcs.TrustworthySW.2006.699,
  author =	{Schaefer, Ina and Poetzsch-Heffter, Arnd},
  title =	{{Using Abstraction in Modular Verification of Synchronous Adaptive Systems}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.699},
  URN =		{urn:nbn:de:0030-drops-6996},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.699},
  annote =	{Keywords: Dependable Embedded Systems, Self-Adaptation, Abstraction, Modular Verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact